ABS: FinProbSpace

STM: finite-prob-space wf

STM: fps-not-null

ABS: *1*

STM: unit-fps wf

ABS: *50/50*

STM: binary-fps wf

ABS: *1/3*

STM: ternary-fps wf

ABS: Outcome

STM: p-outcome wf

STM: natural number wf p-outcome

STM: decidable p-outcome

ABS: weighted-sum(p;F)

STM: weighted-sum wf

ABS: ws_nil{ws_nil_compseq_tag_def:ObjectId}(F)

ABS: ws_single{ws_single_compseq_tag_def:ObjectId}(F; p)

STM: weighted-sum-nil

STM: weighted-sum-split

STM: weighted-sum-linear

STM: ws-monotone

STM: weighted-sum wf2

STM: ws-linear

STM: ws-constant

STM: ws-lower-bound

ABS: null

STM: null-seq wf

ABS: cons-seq(x;s)

STM: cons-seq wf

ABS: RandomVariable(p;n)

STM: random-variable wf

ABS: X + Y

STM: rv-add wf

ABS: q*X

STM: rv-scale wf

ABS: X * Y

STM: rv-mul wf

ABS: rv-shift(x;X)

STM: rv-shift wf

STM: rv-shift-linear

ABS: X@i

STM: rv-sample wf

ABS: A  B

STM: rv-qle wf

ABS: rv-const(a)

STM: rv-const wf

ABS: E(n;F)

STM: expectation wf

STM: expectation-linear

STM: expectation-constant

STM: expectation-rv-const

STM: expectation-rv-add

STM: expectation-rv-scale

STM: expectation-qsum

STM: expectation-rv-sample

ABS: rv-disjoint(p;n;X;Y)

STM: rv-disjoint wf

STM: rv-disjoint-rv-shift

STM: rv-disjoint-rv-add

STM: rv-disjoint-symmetry

STM: rv-disjoint-rv-add2

STM: rv-disjoint-rv-mul

STM: rv-disjoint-rv-mul2

STM: rv-disjoint-const

STM: rv-disjoint-monotone-in-first

ABS: (x.F(x)) o X

STM: rv-compose wf

STM: rv-disjoint-compose

STM: rv-disjoint-rv-scale

STM: rv-disjoint-shift

STM: expectation-rv-disjoint

STM: expectation-rv-add-squared

STM: expectation-rv-add-cubed

STM: expectation-rv-add-fourth

ABS: X  Y

STM: rv-le wf

STM: expectation-monotone

STM: Markov-inequality

STM: expectation-imax-list

STM: expectation-non-neg

ABS: p-open(p)

STM: p-open wf

ABS: s  C

STM: p-open-member wf

ABS: measure(C)  q

STM: p-measure-le wf

STM: open-expectation-monotone

ABS: measure(C) = 1

STM: p-open-measure-one wf

STM: expectation-monotone-in-first

ABS: p-union(A;B)

STM: p-union wf

STM: member-p-union

ABS: countable-p-union(i.A(i))

STM: countable-p-union wf

STM: member-countable-p-union

ABS: nullset(p;S)

STM: nullset wf

ABS: Konig(k)

STM: Konig wf

STM: not-nullset

STM: nullset-union

STM: nullset-monotone

ABS: (X(n) as n)

STM: rv-unbounded wf

STM: bounded-expectation

ABS: rv-identically-distributed(p;n.f(n);i.X(i))

STM: rv-identically-distributed wf

ABS: rv-iid(p;n.f(n);i.X(i))

STM: rv-iid wf

STM: rv-iid-add

STM: rv-iid-add-const

ABS: rv-partial-sum(n;i.X(i))

STM: rv-partial-sum wf

STM: rv-partial-sum-unroll

STM: rv-disjoint-rv-partial-sum

STM: rv-partial-sum-monotone

STM: slln-lemma1

STM: slln-lemma2

STM: slln-lemma3

STM: slln-lemma4

STM: strong-law-of-large-numbers

ABS: random(p;a;b)

STM: random wf

ABS: find-random{$k}(C;p;a;b)

STM: find-random wf

STM: randomness